es:event_system{i:l}, e:es-E(es), x,free:Id.
es-dtype(es; loc(e); x; Id)  (f-rank{i:l}(x; free; es; e)  (:  )) 

latex

Definitions

t  T, #$n, x:A. B(x), A  B, a < b, void, x:AB(x), P  Q, False, A, {x:A| B(x)} , , , <a, b>, b, b, , s = t, prop{i:l}, x:A  B(x), inc-snd(p), loc(e), es-vartype(es; i; x), P  Q, es-dtype(es; i; x; T), es-after(es; x; e), Type, inc-fst(p), eq_id(a; b), left + right, P  Q, Unit, x. t(x), let x = a in b(x), if b then t else f fi , EqDecider(T), event_system{i:l}, let x,y = A in B(x;y), t.1, es-E(es), atom{$n:n}, case b of inl(x) => s(x) | inr(y) => t(y), A c B, f(a), f-rank{i:l}(x; free; es; e), x.A(x), x changed before e, True, T, es-locl(es; e; e'), x:A. B(x), SWellFounded(R(x;y)), ge(i; j), -n, n + m, n - m, id-deq, Id, (last change to x before e)

Lemmas

ge wf, nat properties, event system wf, es-locl-swellfnd, es-locl wf, es-E wf, changed wf, last-change wf, last-change-property, loc-last-change, id-deq wf, deq wf, es-dtype wf, ifthenelse wf, let wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, inc-fst wf, false wf, es-after wf, es-vartype wf, es-loc wf, subtype rel self, Id wf, inc-snd wf, nat wf, bool wf, bnot wf, not wf, assert wf, le wf